cff91a2a41f10597c18095410b2d9606054f9de7,VUE2/src/tufts/vue/URLResource.java,URLResource,makeURI,#File#,405
Before Change
public static URI makeURI(File f) {
URI uri = f.toURI();
Util.dumpURI(uri, "NEW FILE URI FROM " + f);
if (uri.getPath().startsWith("/C:"))
return makeURI(uri.getPath().substring(3));
else
After Change
public static URI makeURI(File f) {
URI uri = f.toURI();
if (DEBUG.RESOURCE) Util.dumpURI(uri, "NEW FILE URI FROM " + f);
if (uri.getPath().startsWith("/C:"))
return makeURI(uri.getPath().substring(3));
else